es:ES, T:Type, I:MaInterface(T), i:Id.
ma-interface-consistent(es;I)  (i  ma-interface-locs(I))  ([[I|i]]  AbsInterface(T)) 

latex

Definitions

x:A. B(x), P  Q, t  T, [[I|i]], f(x), t.2, ma-interface-ds(I;i), t.1, x. t(x), S  T, , Top, a:A fp B(a), P & Q, x:A. B(x), State(ds), state@i, SQType(T), {T}, (x  l), Knd, A c B, A  B, A, False, MaInterface(T), ma-interface-consistent(es;X), ma-interface-locs(I), x  dom(f), ma-interface-consistent-at(es;i;X), fpf-domain(f), P  Q, P  Q, x(s), e@i. P(e),

Lemmas

l member wf, Id wf, ma-interface-locs wf, ma-interface-consistent wf, ma-interface wf, event system wf, assert-deq-member, id-deq wf, fpf wf, Knd wf, assert wf, hasloc wf, decl-state wf, top wf, l member type, decidable assert, l member in subtype2, subtype rel function, es-triggers wf, fpf-dom wf, Kind-deq wf, es-kind wf, es-loc wf, es-E wf, Id sq, es-state-subtype, es-vartype wf, fpf-cap wf, IdLnk wf, alle-at wf, pi1 wf, nat wf, length wf1, select wf